Termination Proof Script

Consider the TRS R consisting of the rewrite rule


1:	app(app(iterate,f),x)	→ app(app(cons,x),app(app(iterate,f),app(f,x)))

There are 4 dependency pairs:


2:	APP(app(iterate,f),x)	→ APP(app(cons,x),app(app(iterate,f),app(f,x)))
3:	APP(app(iterate,f),x)	→ APP(cons,x)
4:	APP(app(iterate,f),x)	→ APP(app(iterate,f),app(f,x))
5:	APP(app(iterate,f),x)	→ APP(f,x)

The approximated dependency graph contains one SCC: {2,4,5}.

Tyrolean Termination Tool (0.03 seconds) --- May 4, 2006